es:ES, ff:FIFO. ff.Sender  i:ff.C{e:E| ff.R(i,e)} {e:E| j:ff.C. (ff.S(j,i,e))}  

latex

Definitions	x:A. B(x), t  T, ff.C, ff.R, x:A. B(x), ff.S, ff.Sender, , let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), P & Q, P  Q, x. t(x), A c B, FIFO, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), x(s)
Lemmas	pi1 wf, es-causle wf, FIFO wf, event system wf